Section: Software

Coqfinitgroup

Participants : Cyril Cohen, Assia Mahboubi [Contact] .

Coqfinitegroup is the development corresponding to the ongoing effort to formalize the proof of the Feit-Thompson theorem. It is probably the most advanced formal development of group theory today. Its current size is about 80.000 lines of (compact) Coq code. Assia Mahboubi and Cyril Cohen are actively participating to this long term formalization project.